Nuprl Lemma : safety_wf
4,23
postcript
pdf
A
:Type,
P
:((
A
List)
Prop). safety(
A
;
x
.
P
(
x
))
Prop
latex
Definitions
t
T
,
Prop
,
x
(
s
)
,
P
Q
,
x
:
A
.
B
(
x
)
,
l1
l2
,
safety(
A
;
tr
.
P
(
tr
))
Lemmas
iseg
wf
origin
A:Type, P:((A List)
Prop). safety(A;x.P(x)) 
Prop A:Type, P:((A List)Prop). safety(A;x.P(x)) Prop T
Qx:A. B(x)
l2